Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(.,1),x)  → x
2:    app(app(.,x),1)  → x
3:    app(app(.,app(i,x)),x)  → 1
4:    app(app(.,x),app(i,x))  → 1
5:    app(app(.,app(i,y)),app(app(.,y),z))  → z
6:    app(app(.,y),app(app(.,app(i,y)),z))  → z
7:    app(app(.,app(app(.,x),y)),z)  → app(app(.,x),app(app(.,y),z))
8:    app(i,1)  → 1
9:    app(i,app(i,x))  → x
10:    app(i,app(app(.,x),y))  → app(app(.,app(i,y)),app(i,x))
There are 7 dependency pairs:
11:    APP(app(.,app(app(.,x),y)),z)  → APP(app(.,x),app(app(.,y),z))
12:    APP(app(.,app(app(.,x),y)),z)  → APP(app(.,y),z)
13:    APP(app(.,app(app(.,x),y)),z)  → APP(.,y)
14:    APP(i,app(app(.,x),y))  → APP(app(.,app(i,y)),app(i,x))
15:    APP(i,app(app(.,x),y))  → APP(.,app(i,y))
16:    APP(i,app(app(.,x),y))  → APP(i,y)
17:    APP(i,app(app(.,x),y))  → APP(i,x)
The approximated dependency graph contains one SCC: {11,12,14,16,17}.
Tyrolean Termination Tool  (0.04 seconds)   ---  May 3, 2006